(set-logic QF_UFLIRAFS)
(set-info :status sat)
(declare-fun s () (Set Real))
(declare-fun t1 () (Set Real))
(declare-fun t2 () (Set Real))
(declare-fun t3 () (Set Real))
(declare-fun r1 () (Set Real))
(declare-fun r2 () (Set Real))
(declare-fun r3 () (Set Real))
(assert (and (set.member 1.5 s) (set.member 0.0 s)))
(assert (= t1 (set.union s (set.singleton 2.5))))
(assert (= t2 (set.union s (set.singleton 2.0))))
(assert (= t3 (set.union r3 (set.singleton 2.5))))
(assert (= (set.inter r1 r2) (set.inter s (set.singleton 0.0))))
(assert (not (= r1 (as set.empty (Set Real)))))

(check-sat)
